COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00013 00003	.skip 1
C00014 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.CB EXPRESSION OF MODALITY IN FIRST ORDER LOGIC


	For reasons that will be explained, I think artificial
intelligence requires modalities
such as possibility, necessity, knowledge, belief, obligation
and futurity, but I think modal logic is not a good framework
for expressing them.  The object of these
notes is to describe a way of expressing modal statements in
ordinary first order logic.  In the first section, we will
translate the language of propositional modal logic into
first order logic.  We will mainly be covering familiar ground;
our formulas will be somewhat longer than the corresponding
formulas of modal logic.

	In the second section, I will give an application to
formalizing some puzzles involving knowledge which I don't think
are feasible in unadorned modal logic.  Anyway they haven't been
done.

	In the third section, I will discuss some of the issues
of formalization of modalities in a general way.

.item←0
#. Propositions and the first order theory MODAL1

	We introduce a sort of entities called %2propositions%1
and use ⊗P, ⊗P0, ⊗P1, ⊗P2, etc. and ⊗Q, ⊗Q0, etc. as variables
denoting propositions.  There is a predicate of propositions
called ⊗true, and %2true_P%1 is the assertion that the proposition
⊗P is true.  From propositions we can get other propositions by
functions imitating the Boolean operators.  Thus we have %2not_P%1,
%2P_and_Q%1, %2P_or_Q%1, and %2P_implies_Q%1, etc.  Finally, we
have the modal functions %2Nec_P%1 and %2Poss_P%1.  The following
are axioms:

!!a1:	%2∀P.(true not P ≡ ¬true P)%1,

!!a2:	%2∀P Q.(true (P and Q) ≡ true P ∧ true Q)%1,

!!a3:	%2∀P Q.(true (P or Q) ≡ true P ∨ true Q)%1,

!!a4:	%2∀P Q.(true (P implies Q) ≡ true P ⊃ true Q)%1,

and

!!a4a:	%2∀P Q.(true (P equiv Q) ≡ (true P ≡ true Q))%1,

etc., for any additional Boolean operators that may be wanted.

	So far not much has happened, because we haven't done
anything with our imitation Boolean operators that couldn't be
done without them.  Indeed if we were to use the systematic
notational convention

	%2p = true P%1,

then any formula involving ⊗true applied to some combination of
proposition letters with the imitation Boolean operators could
be rewritten in terms of the %2p%1's and ordinary Boolean operators.
We get something new when we introduce the axioms satisfied by the
modal operators

!!a5:	%2∀P.true(Nec P implies P)%1,

!!a5a:	%2∀P.true Nec (Nec P implies P)%1,

!!a51:	%2∀P Q.true Nec (Nec P and Nec Q implies Nec(P and Q))%1,

and

!!a52:	%2VP Q.true Nec (Nec P and Nec(P implies Q) implies Nec Q)%1

together with the necessity of your favorite set of axioms for the
propositional calculus, e.g. the formulas

!!a54:	%2∀P.Nec((P or P) implies P)%1,

!!a53:	%2∀P Q.Nec(Q implies (P or Q))%1,

!!a55:	%2∀P Q.Nec((P or Q) implies (Q or P))%1,

and

!!a56:	%2∀P Q R.Nec((Q implies R) implies ((P or Q) implies (P or R)))%1,

which we have copied from (Hughes and Cresswell 1968) who copied them
from Whitehead and Russell's %2Principia Mathematica%1.

We also have

!!a6:	%2∀P.true(Poss P equiv not Nec not P)%1.

	With just these axioms, we have a system equivalent to
M in the sense that a sentence of MODAL1 can be proved if and
only if the corresponding sentence of M can be proved.
S4 is given by adjoining to the above axioms

!!a7:	%2∀P.true (Nec P implies Nec Nec P)%1,

and S5 is given by adjoining

!!a8:	%2∀P.true (Poss P implies Nec Poss P)%1.


#. Kripke Semantics

	We get the Kripke semantics by introducing another sort called
possible worlds, and we use variables ⊗w, ⊗w0, ⊗w1, etc. for them.
We have a relation ⊗a(w1,w2) saying that the world ⊗w2 is possible
(or accessible)
from the world ⊗w1.  We extend the predicate ⊗true to take a world
as a second argument so that we have ⊗true(P,w), and we introduce
a preferred world called ⊗RW (the real world) and identify
⊗true_P and ⊗true(P,RW).  The propositional axioms are extended in
the obvious way so that we have
such axioms as

!!a9:	%2∀P Q w.(true(P and Q,w) ≡ true(P,w) ∧ true(Q,w))%1

analogous to ({eq a2}) and similar axioms analogous to the others.

	The truth of the modal functions Nec and Poss is determined by
the axioms

!!a10:	%2∀P w.(true(Nec P,w) ≡ ∀w1.(a(w,w1) ⊃ true(P,w1))%1

and

!!a11:	%2∀P w.(true(Poss P,w) ≡ ∃w1.(a(w,w1) ∧ true(P,w1))%1.

	The reflexivity of ⊗a as expressed by

!!a12:	%2∀w.a(w,w)%1

is equivalent to ({eq a5}).  S4 is obtained by making ⊗a transitive, i.e.

!!a13:	%2∀w1 w2 w3.(a(w1,w2) ∧ a(w2,w3) ⊃ a(w1,w3))%1,

and S5 is obtained by adjoining

!!a14:	%2∀w1 w2.(a(w1,w2) ⊃ a(w2,w1))%1

so as to make ⊗a an equivalence relation.

	The advantages and disadvantages of the predicate calculus
treatment over the modal logic treatment seem so far to be a matter
of taste.  The traditional treatment modifies the logic which is
a nuisance for people who experiment with predicate calculus theorem
provers or proof checkers.  On the other hand, one may feel that
quantifiers are more complicated than modal operators.
Treating quantified modal logic might give more information about
whether the predicate calculus treatment is preferable, but we
haven't tried that yet.  Instead we have worked on formulating some
puzzles in the logic of knowledge.  There we know how to do some
things that are required for solving the puzzles in the predicate
calculus treatment using possible worlds, and we don't yet know
how to do them in modal logic.


#. Knowledge as a modal operator

	Many philosophical authors have treated knowledge using modal
operators.  (Hintikka 1962) is a major reference and the Kripke
semantics of modal logic is extensively discussed in Sato's (1977)
thesis.  The main formal emphasis has been on "knowing that" where
the operand is a sentence or proposition, and the non-mathematical
philosophers
have emphasized the importance of "knowing how", although it hasn't
been treated formally.  In order to solve the puzzles we shall discuss
in this section, it is important to emphasize "knowing what", e.g.
%2"Pat knows Mike's telephone number"%1 or %2"The second wiseman
doesn't know the color of his spot"%1.

	We shall emphasize semantic treatments and introduce a new
accessibilty relation %2A(w1,w2,person,time)%1 which means that world
⊗w2 is accessible (possible) from world ⊗w1 for person ⊗person at
time ⊗time.  We introduce time, because our puzzles involve people
learning things.

(to be continued)
.skip 1
.begin verbatim
John McCarthy
Artificial Intelligence Laboratory
Computer Science Department
Stanford University
Stanford, California 94305

ARPANET: MCCARTHY@SU-AI
.end

.turn on "{"
%7This draft of
MODAL[S78,JMC]
PUBbed at {time} on {date}.%1